$\forall$$T$, ${\it T'}$:Type, $x$:${\it T'}$, $a$:Atom1.
\\[0ex]AtomFree(Type;$T$) $\Rightarrow$ AtomFree(Type;${\it T'}$) $\Rightarrow$ $x$:${\it T'}$$>>$$a$ $\Rightarrow$ inr($x$):$T$+${\it T'}$$>>$$a$